YES 184.536
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((isAlphaNum :: Char -> Bool) :: Char -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((isAlphaNum :: Char -> Bool) :: Char -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule Main
| ((isAlphaNum :: Char -> Bool) :: Char -> Bool) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
| (isAlphaNum :: Char -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_not(Succ(vx3160), Succ(vx3180)) → new_not(vx3160, vx3180)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_not(Succ(vx3160), Succ(vx3180)) → new_not(vx3160, vx3180)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_asAs(Succ(vx3160000), Succ(vx3170000), vx320) → new_asAs(vx3160000, vx3170000, vx320)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_asAs(Succ(vx3160000), Succ(vx3170000), vx320) → new_asAs(vx3160000, vx3170000, vx320)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe(Succ(vx3090), Succ(vx3100), vx311) → new_pePe(vx3090, vx3100, vx311)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe(Succ(vx3090), Succ(vx3100), vx311) → new_pePe(vx3090, vx3100, vx311)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe0(Succ(vx3070), Succ(vx3080), vx309, vx310) → new_pePe0(vx3070, vx3080, vx309, vx310)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe0(Succ(vx3070), Succ(vx3080), vx309, vx310) → new_pePe0(vx3070, vx3080, vx309, vx310)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe1(Succ(vx2990), Succ(vx3000), vx301, vx302, vx303) → new_pePe1(vx2990, vx3000, vx301, vx302, vx303)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe1(Succ(vx2990), Succ(vx3000), vx301, vx302, vx303) → new_pePe1(vx2990, vx3000, vx301, vx302, vx303)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe2(Succ(vx2810), Succ(vx2820), vx283, vx284, vx285, vx286) → new_pePe2(vx2810, vx2820, vx283, vx284, vx285, vx286)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe2(Succ(vx2810), Succ(vx2820), vx283, vx284, vx285, vx286) → new_pePe2(vx2810, vx2820, vx283, vx284, vx285, vx286)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe3(Succ(vx2730), Succ(vx2740), vx275, vx276, vx277, vx278, vx279) → new_pePe3(vx2730, vx2740, vx275, vx276, vx277, vx278, vx279)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe3(Succ(vx2730), Succ(vx2740), vx275, vx276, vx277, vx278, vx279) → new_pePe3(vx2730, vx2740, vx275, vx276, vx277, vx278, vx279)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe4(Succ(vx2640), Succ(vx2650), vx266, vx267, vx268, vx269, vx270, vx271) → new_pePe4(vx2640, vx2650, vx266, vx267, vx268, vx269, vx270, vx271)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe4(Succ(vx2640), Succ(vx2650), vx266, vx267, vx268, vx269, vx270, vx271) → new_pePe4(vx2640, vx2650, vx266, vx267, vx268, vx269, vx270, vx271)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe5(Succ(vx2530), Succ(vx2540), vx255) → new_pePe5(vx2530, vx2540, vx255)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe5(Succ(vx2530), Succ(vx2540), vx255) → new_pePe5(vx2530, vx2540, vx255)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe6(Succ(vx1980), Succ(vx1990), vx200, vx201) → new_pePe6(vx1980, vx1990, vx200, vx201)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe6(Succ(vx1980), Succ(vx1990), vx200, vx201) → new_pePe6(vx1980, vx1990, vx200, vx201)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe7(Succ(vx2030), Succ(vx2040), vx205, vx206, vx207) → new_pePe7(vx2030, vx2040, vx205, vx206, vx207)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe7(Succ(vx2030), Succ(vx2040), vx205, vx206, vx207) → new_pePe7(vx2030, vx2040, vx205, vx206, vx207)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe8(Succ(vx1220), Succ(vx1230), vx124, vx125, vx126, vx127) → new_pePe8(vx1220, vx1230, vx124, vx125, vx126, vx127)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe8(Succ(vx1220), Succ(vx1230), vx124, vx125, vx126, vx127) → new_pePe8(vx1220, vx1230, vx124, vx125, vx126, vx127)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_pePe9(Succ(vx1120), Succ(vx1130), vx114, vx115, vx116, vx117, vx118) → new_pePe9(vx1120, vx1130, vx114, vx115, vx116, vx117, vx118)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe9(Succ(vx1120), Succ(vx1130), vx114, vx115, vx116, vx117, vx118) → new_pePe9(vx1120, vx1130, vx114, vx115, vx116, vx117, vx118)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_pePe10(Succ(vx600), Succ(vx610), vx62, vx63, vx64, vx65, vx66, vx67) → new_pePe10(vx600, vx610, vx62, vx63, vx64, vx65, vx66, vx67)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_pePe10(Succ(vx600), Succ(vx610), vx62, vx63, vx64, vx65, vx66, vx67) → new_pePe10(vx600, vx610, vx62, vx63, vx64, vx65, vx66, vx67)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8